(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 1))
(let ((e4 1))
(let ((e5 (- v2 v1)))
(let ((e6 (* v1 v1)))
(let ((e7 (* e4 e5)))
(let ((e8 (- e7 e5)))
(let ((e9 (- v2)))
(let ((e10 (- v2)))
(let ((e11 (- e9 v2)))
(let ((e12 (+ e11 e6)))
(let ((e13 (- e6 e10)))
(let ((e14 (- e7)))
(let ((e15 (* e11 e3)))
(let ((e16 (- v1)))
(let ((e17 (/ e3 (- e3))))
(let ((e18 (- e10)))
(let ((e19 (- e11)))
(let ((e20 (+ e17 e18)))
(let ((e21 (- e12)))
(let ((e22 (/ e4 (- e4))))
(let ((e23 (- e9)))
(let ((e24 (+ e23 e16)))
(let ((e25 (* (- e3) v0)))
(let ((e26 (> e11 e14)))
(let ((e27 (distinct e6 e24)))
(let ((e28 (distinct v2 v1)))
(let ((e29 (>= e19 v0)))
(let ((e30 (= v0 e11)))
(let ((e31 (> e9 e12)))
(let ((e32 (<= e14 e15)))
(let ((e33 (< e23 e22)))
(let ((e34 (= e14 v2)))
(let ((e35 (> e12 e5)))
(let ((e36 (= e9 e18)))
(let ((e37 (> e19 e10)))
(let ((e38 (<= e11 e22)))
(let ((e39 (< e20 e14)))
(let ((e40 (< e22 e22)))
(let ((e41 (> e10 e20)))
(let ((e42 (> e5 e6)))
(let ((e43 (= e7 e21)))
(let ((e44 (= e23 e16)))
(let ((e45 (< e19 e19)))
(let ((e46 (distinct v0 e6)))
(let ((e47 (distinct e19 e23)))
(let ((e48 (>= e16 e19)))
(let ((e49 (= e24 e14)))
(let ((e50 (distinct e22 e17)))
(let ((e51 (> e22 e15)))
(let ((e52 (= e5 e9)))
(let ((e53 (= e17 e15)))
(let ((e54 (<= e17 e13)))
(let ((e55 (<= e7 e20)))
(let ((e56 (< e19 e19)))
(let ((e57 (= e12 v2)))
(let ((e58 (distinct e20 e8)))
(let ((e59 (> e15 v2)))
(let ((e60 (<= v1 e22)))
(let ((e61 (> e19 e12)))
(let ((e62 (< e9 v1)))
(let ((e63 (> v2 e17)))
(let ((e64 (= e16 e15)))
(let ((e65 (distinct e11 v0)))
(let ((e66 (distinct e25 v1)))
(let ((e67 (<= e12 e23)))
(let ((e68 (< e25 e16)))
(let ((e69 (<= e20 e8)))
(let ((e70 (>= e23 e22)))
(let ((e71 (<= e9 e15)))
(let ((e72 (> e25 e16)))
(let ((e73 (> v0 e10)))
(let ((e74 (distinct v0 e17)))
(let ((e75 (>= e6 e11)))
(let ((e76 (distinct v2 e9)))
(let ((e77 (>= e23 e13)))
(let ((e78 (> e17 e24)))
(let ((e79 (< e21 e22)))
(let ((e80 (>= e12 e19)))
(let ((e81 (> v0 e10)))
(let ((e82 (distinct e15 e23)))
(let ((e83 (<= e19 e15)))
(let ((e84 (> e17 e15)))
(let ((e85 (>= e25 e20)))
(let ((e86 (<= e7 e21)))
(let ((e87 (= e10 e18)))
(let ((e88 (distinct e23 e6)))
(let ((e89 (< e7 e19)))
(let ((e90 (>= e25 e16)))
(let ((e91 (distinct v0 e12)))
(let ((e92 (distinct e16 e16)))
(let ((e93 (distinct v0 e20)))
(let ((e94 (= e19 v0)))
(let ((e95 (distinct v2 e9)))
(let ((e96 (>= e10 e9)))
(let ((e97 (< e11 e23)))
(let ((e98 (= e19 e19)))
(let ((e99 (>= e20 e20)))
(let ((e100 (<= e19 e15)))
(let ((e101 (> e11 e19)))
(let ((e102 (<= e17 e24)))
(let ((e103 (< e17 e10)))
(let ((e104 (distinct e24 e15)))
(let ((e105 (distinct e6 e17)))
(let ((e106 (>= e19 e24)))
(let ((e107 (> e12 v1)))
(let ((e108 (>= e21 e22)))
(let ((e109 (<= e7 v1)))
(let ((e110 (< e8 e24)))
(let ((e111 (>= v0 e22)))
(let ((e112 (> e22 e12)))
(let ((e113 (<= e16 e7)))
(let ((e114 (distinct e22 e12)))
(let ((e115 (< e22 e16)))
(let ((e116 (distinct e20 v0)))
(let ((e117 (> e5 e21)))
(let ((e118 (distinct e16 e13)))
(let ((e119 (= e23 e17)))
(let ((e120 (< v1 e5)))
(let ((e121 (> v2 e17)))
(let ((e122 (>= e24 e17)))
(let ((e123 (distinct e10 e19)))
(let ((e124 (distinct e16 v2)))
(let ((e125 (= e11 e7)))
(let ((e126 (distinct v0 e5)))
(let ((e127 (distinct e5 e8)))
(let ((e128 (<= e8 e19)))
(let ((e129 (> e22 e18)))
(let ((e130 (= e10 e8)))
(let ((e131 (< e17 e7)))
(let ((e132 (> e19 v1)))
(let ((e133 (< e18 e24)))
(let ((e134 (distinct e12 e25)))
(let ((e135 (distinct e18 e11)))
(let ((e136 (distinct e22 e17)))
(let ((e137 (< v1 e21)))
(let ((e138 (< e18 e16)))
(let ((e139 (= e5 e25)))
(let ((e140 (= e7 e19)))
(let ((e141 (>= e23 e17)))
(let ((e142 (< v1 e25)))
(let ((e143 (= e6 v1)))
(let ((e144 (<= e11 e18)))
(let ((e145 (= e6 e8)))
(let ((e146 (> e15 e12)))
(let ((e147 (<= v2 e21)))
(let ((e148 (< v1 e25)))
(let ((e149 (<= e23 e13)))
(let ((e150 (< e8 e17)))
(let ((e151 (< e18 v2)))
(let ((e152 (<= e5 e12)))
(let ((e153 (>= e24 e10)))
(let ((e154 (= e19 e25)))
(let ((e155 (> v2 e22)))
(let ((e156 (<= e23 e21)))
(let ((e157 (> e9 e24)))
(let ((e158 (distinct v2 e8)))
(let ((e159 (> v1 v1)))
(let ((e160 (= e5 e9)))
(let ((e161 (< e6 e15)))
(let ((e162 (>= e8 e22)))
(let ((e163 (< e14 e14)))
(let ((e164 (and e48 e131)))
(let ((e165 (= e50 e109)))
(let ((e166 (xor e136 e36)))
(let ((e167 (not e140)))
(let ((e168 (=> e130 e76)))
(let ((e169 (and e150 e108)))
(let ((e170 (not e158)))
(let ((e171 (ite e157 e85 e107)))
(let ((e172 (= e139 e147)))
(let ((e173 (and e57 e111)))
(let ((e174 (= e75 e87)))
(let ((e175 (=> e151 e30)))
(let ((e176 (not e115)))
(let ((e177 (= e160 e145)))
(let ((e178 (or e86 e94)))
(let ((e179 (ite e81 e44 e126)))
(let ((e180 (= e74 e45)))
(let ((e181 (or e176 e65)))
(let ((e182 (=> e169 e72)))
(let ((e183 (xor e180 e143)))
(let ((e184 (ite e43 e102 e101)))
(let ((e185 (=> e64 e99)))
(let ((e186 (or e97 e27)))
(let ((e187 (and e37 e42)))
(let ((e188 (or e144 e163)))
(let ((e189 (= e116 e187)))
(let ((e190 (not e63)))
(let ((e191 (or e32 e179)))
(let ((e192 (and e112 e175)))
(let ((e193 (= e90 e71)))
(let ((e194 (= e70 e46)))
(let ((e195 (or e164 e84)))
(let ((e196 (=> e174 e51)))
(let ((e197 (not e129)))
(let ((e198 (not e39)))
(let ((e199 (not e127)))
(let ((e200 (or e68 e66)))
(let ((e201 (= e149 e167)))
(let ((e202 (=> e186 e155)))
(let ((e203 (and e138 e88)))
(let ((e204 (or e47 e171)))
(let ((e205 (ite e142 e133 e53)))
(let ((e206 (xor e148 e152)))
(let ((e207 (=> e34 e185)))
(let ((e208 (xor e67 e93)))
(let ((e209 (=> e114 e205)))
(let ((e210 (and e122 e191)))
(let ((e211 (= e38 e135)))
(let ((e212 (xor e106 e58)))
(let ((e213 (and e104 e59)))
(let ((e214 (and e123 e189)))
(let ((e215 (not e211)))
(let ((e216 (= e156 e165)))
(let ((e217 (or e196 e125)))
(let ((e218 (= e178 e89)))
(let ((e219 (not e193)))
(let ((e220 (=> e26 e213)))
(let ((e221 (xor e220 e141)))
(let ((e222 (or e79 e173)))
(let ((e223 (or e207 e200)))
(let ((e224 (or e216 e219)))
(let ((e225 (xor e73 e29)))
(let ((e226 (not e217)))
(let ((e227 (and e54 e192)))
(let ((e228 (or e154 e223)))
(let ((e229 (or e227 e124)))
(let ((e230 (=> e210 e56)))
(let ((e231 (not e41)))
(let ((e232 (and e137 e206)))
(let ((e233 (=> e229 e224)))
(let ((e234 (xor e233 e80)))
(let ((e235 (not e132)))
(let ((e236 (not e113)))
(let ((e237 (and e181 e103)))
(let ((e238 (xor e118 e100)))
(let ((e239 (=> e49 e153)))
(let ((e240 (= e239 e120)))
(let ((e241 (xor e82 e182)))
(let ((e242 (ite e197 e91 e236)))
(let ((e243 (not e198)))
(let ((e244 (= e31 e134)))
(let ((e245 (xor e168 e232)))
(let ((e246 (= e226 e222)))
(let ((e247 (and e221 e208)))
(let ((e248 (xor e238 e246)))
(let ((e249 (ite e83 e244 e245)))
(let ((e250 (xor e98 e119)))
(let ((e251 (and e172 e110)))
(let ((e252 (=> e235 e225)))
(let ((e253 (=> e28 e243)))
(let ((e254 (xor e195 e253)))
(let ((e255 (xor e159 e234)))
(let ((e256 (= e254 e33)))
(let ((e257 (= e117 e240)))
(let ((e258 (and e40 e249)))
(let ((e259 (xor e162 e78)))
(let ((e260 (=> e55 e251)))
(let ((e261 (or e231 e248)))
(let ((e262 (=> e170 e77)))
(let ((e263 (ite e201 e188 e241)))
(let ((e264 (ite e237 e242 e166)))
(let ((e265 (xor e128 e256)))
(let ((e266 (xor e212 e105)))
(let ((e267 (=> e266 e190)))
(let ((e268 (not e199)))
(let ((e269 (or e61 e257)))
(let ((e270 (or e177 e255)))
(let ((e271 (= e218 e203)))
(let ((e272 (=> e259 e184)))
(let ((e273 (not e69)))
(let ((e274 (not e96)))
(let ((e275 (and e62 e95)))
(let ((e276 (or e275 e262)))
(let ((e277 (ite e121 e264 e252)))
(let ((e278 (= e274 e277)))
(let ((e279 (= e278 e276)))
(let ((e280 (= e230 e209)))
(let ((e281 (=> e92 e146)))
(let ((e282 (and e279 e273)))
(let ((e283 (or e194 e228)))
(let ((e284 (or e283 e267)))
(let ((e285 (=> e280 e258)))
(let ((e286 (xor e270 e269)))
(let ((e287 (= e52 e35)))
(let ((e288 (ite e268 e272 e284)))
(let ((e289 (ite e204 e183 e281)))
(let ((e290 (and e263 e214)))
(let ((e291 (not e287)))
(let ((e292 (= e286 e161)))
(let ((e293 (= e292 e292)))
(let ((e294 (= e293 e60)))
(let ((e295 (and e290 e294)))
(let ((e296 (xor e265 e265)))
(let ((e297 (not e288)))
(let ((e298 (not e202)))
(let ((e299 (= e282 e261)))
(let ((e300 (and e291 e247)))
(let ((e301 (xor e289 e295)))
(let ((e302 (= e250 e271)))
(let ((e303 (xor e299 e301)))
(let ((e304 (= e215 e302)))
(let ((e305 (or e297 e303)))
(let ((e306 (=> e296 e300)))
(let ((e307 (xor e304 e305)))
(let ((e308 (not e260)))
(let ((e309 (= e306 e308)))
(let ((e310 (=> e307 e307)))
(let ((e311 (ite e310 e310 e285)))
(let ((e312 (or e298 e298)))
(let ((e313 (= e311 e309)))
(let ((e314 (not e312)))
(let ((e315 (and e314 e314)))
(let ((e316 (not e315)))
(let ((e317 (=> e313 e316)))
e317
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
